eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
↳ QTRS
↳ DependencyPairsProof
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
IF_MINSORT(true, add(n, x), y) → RM(n, x)
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_RM(false, n, add(m, x)) → RM(n, x)
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
IF_MINSORT(true, add(n, x), y) → APP(rm(n, x), y)
LE(s(x), s(y)) → LE(x, y)
IF_MINSORT(true, add(n, x), y) → MINSORT(app(rm(n, x), y), nil)
MINSORT(add(n, x), y) → EQ(n, min(add(n, x)))
APP(add(n, x), y) → APP(x, y)
MINSORT(add(n, x), y) → MIN(add(n, x))
EQ(s(x), s(y)) → EQ(x, y)
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
RM(n, add(m, x)) → EQ(n, m)
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
MIN(add(n, add(m, x))) → LE(n, m)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IF_MINSORT(true, add(n, x), y) → RM(n, x)
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_RM(false, n, add(m, x)) → RM(n, x)
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
IF_MINSORT(true, add(n, x), y) → APP(rm(n, x), y)
LE(s(x), s(y)) → LE(x, y)
IF_MINSORT(true, add(n, x), y) → MINSORT(app(rm(n, x), y), nil)
MINSORT(add(n, x), y) → EQ(n, min(add(n, x)))
APP(add(n, x), y) → APP(x, y)
MINSORT(add(n, x), y) → MIN(add(n, x))
EQ(s(x), s(y)) → EQ(x, y)
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
RM(n, add(m, x)) → EQ(n, m)
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
MIN(add(n, add(m, x))) → LE(n, m)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
APP(add(n, x), y) → APP(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
APP(add(n, x), y) → APP(x, y)
The value of delta used in the strict ordering is 1/2.
POL(APP(x1, x2)) = (2)x_1
POL(add(x1, x2)) = 1/4 + (7/2)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
LE(s(x), s(y)) → LE(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LE(s(x), s(y)) → LE(x, y)
The value of delta used in the strict ordering is 85/16.
POL(s(x1)) = 5/4 + (15/4)x_1
POL(LE(x1, x2)) = x_1 + (13/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF_MIN(false, add(n, add(m, x))) → MIN(add(m, x))
MIN(add(n, add(m, x))) → IF_MIN(le(n, m), add(n, add(m, x)))
IF_MIN(true, add(n, add(m, x))) → MIN(add(n, x))
The value of delta used in the strict ordering is 15/4.
POL(add(x1, x2)) = 2 + (4)x_2
POL(IF_MIN(x1, x2)) = x_2
POL(le(x1, x2)) = 0
POL(MIN(x1)) = 15/4 + x_1
POL(true) = 4
POL(false) = 0
POL(s(x1)) = 15/4 + (1/2)x_1
POL(0) = 1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
EQ(s(x), s(y)) → EQ(x, y)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
EQ(s(x), s(y)) → EQ(x, y)
The value of delta used in the strict ordering is 85/16.
POL(EQ(x1, x2)) = x_1 + (13/4)x_2
POL(s(x1)) = 5/4 + (15/4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
RM(n, add(m, x)) → IF_RM(eq(n, m), n, add(m, x))
IF_RM(true, n, add(m, x)) → RM(n, x)
IF_RM(false, n, add(m, x)) → RM(n, x)
The value of delta used in the strict ordering is 1.
POL(RM(x1, x2)) = 3 + (4)x_2
POL(add(x1, x2)) = 4 + (4)x_2
POL(eq(x1, x2)) = 0
POL(IF_RM(x1, x2, x3)) = x_3
POL(true) = 0
POL(false) = 0
POL(s(x1)) = 4 + (5/2)x_1
POL(0) = 1/2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
IF_MINSORT(true, add(n, x), y) → MINSORT(app(rm(n, x), y), nil)
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF_MINSORT(true, add(n, x), y) → MINSORT(app(rm(n, x), y), nil)
Used ordering: Polynomial interpretation [25,35]:
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
The value of delta used in the strict ordering is 1/16.
POL(eq(x1, x2)) = 0
POL(MINSORT(x1, x2)) = (1/4)x_1 + (1/4)x_2
POL(le(x1, x2)) = 4 + (7/4)x_1 + (4)x_2
POL(true) = 0
POL(rm(x1, x2)) = (3/4)x_1 + x_2
POL(if_rm(x1, x2, x3)) = (3/4)x_2 + x_3
POL(0) = 0
POL(IF_MINSORT(x1, x2, x3)) = (1/4)x_2 + (1/4)x_3
POL(add(x1, x2)) = 1/4 + (2)x_1 + x_2
POL(false) = 0
POL(app(x1, x2)) = x_1 + x_2
POL(s(x1)) = (4)x_1
POL(min(x1)) = 0
POL(nil) = 0
POL(if_min(x1, x2)) = 3 + (9/4)x_1 + (3/4)x_2
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
rm(n, nil) → nil
if_rm(true, n, add(m, x)) → rm(n, x)
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
app(add(n, x), y) → add(n, app(x, y))
app(nil, y) → y
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MINSORT(add(n, x), y) → IF_MINSORT(eq(n, min(add(n, x))), add(n, x), y)
IF_MINSORT(false, add(n, x), y) → MINSORT(x, add(n, y))
The value of delta used in the strict ordering is 1/4.
POL(add(x1, x2)) = 1 + (4)x_1 + (4)x_2
POL(eq(x1, x2)) = 0
POL(MINSORT(x1, x2)) = 5/4 + (4)x_1
POL(le(x1, x2)) = 0
POL(true) = 4
POL(false) = 4
POL(s(x1)) = 15/4 + (3)x_1
POL(min(x1)) = 5/4 + (1/4)x_1
POL(0) = 5/2
POL(IF_MINSORT(x1, x2, x3)) = 1/2 + x_2
POL(nil) = 0
POL(if_min(x1, x2)) = (4)x_1 + (1/4)x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
eq(0, 0) → true
eq(0, s(x)) → false
eq(s(x), 0) → false
eq(s(x), s(y)) → eq(x, y)
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
min(add(n, nil)) → n
min(add(n, add(m, x))) → if_min(le(n, m), add(n, add(m, x)))
if_min(true, add(n, add(m, x))) → min(add(n, x))
if_min(false, add(n, add(m, x))) → min(add(m, x))
rm(n, nil) → nil
rm(n, add(m, x)) → if_rm(eq(n, m), n, add(m, x))
if_rm(true, n, add(m, x)) → rm(n, x)
if_rm(false, n, add(m, x)) → add(m, rm(n, x))
minsort(nil, nil) → nil
minsort(add(n, x), y) → if_minsort(eq(n, min(add(n, x))), add(n, x), y)
if_minsort(true, add(n, x), y) → add(n, minsort(app(rm(n, x), y), nil))
if_minsort(false, add(n, x), y) → minsort(x, add(n, y))